package de.uka.ilkd.key.dl.arithmetics.impl.metitarski;

import java.util.Arrays;
import java.util.HashSet;
import java.util.TreeSet;
import org.apache.log4j.Logger;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.Op;
import de.uka.ilkd.key.dl.arithmetics.impl.preprocessor.Node;
import de.uka.ilkd.key.dl.arithmetics.impl.preprocessor.Operators;
import de.uka.ilkd.key.dl.arithmetics.impl.preprocessor.Tree;

/**
 * 
 * @author s0805753@sms.ed.ac.uk
 * @since 12/02/2012
 *
 */
public class termToMetitConverter {

	private static Logger logger = Logger.getLogger("MetiTarski Converter Logger");
	
	/* Special function symbols */
	// FIXME: NOT optimal!
	/* N.B. these will (hopefully) be used eventually in classifying problems */
	
	private static final String[] trigSym = {"Sin", "Cos", "Tan"};
	private static final String[] recTrigSym = {"Csc", "Sec", "Cot"};
	private static final String[] invTrigSym = {"ArcSin", "ArcCos", "ArcTan"};
	private static final String[] invRecTrigSym = {"ArcCsc", "ArcSec", "ArcCot"};
	private static final String[] hypTrigSym = {"Sinh", "Cosh", "Tanh"};
	private static final String[] recHypTrigSym = {"Csch", "Sech", "Coth"};
	private static final String[] invHypTrigSym = {"ArcSinh", "ArcCosh", "ArcTanh"};
	private static final String[] invrecHypTrigSym = {"ArcCsch", "ArcSech", "ArcCoth"};
	private static final String[] expLog = {"Exp", "Log" };

	static HashSet<String> specialFunctionSymbols = unionOf(trigSym, recTrigSym,
			invTrigSym, invRecTrigSym, hypTrigSym, recHypTrigSym,
			invHypTrigSym, invrecHypTrigSym, expLog);

	/* Set membership and union */
	
	static boolean containsElement(String[] set, String element) {
		return Arrays.asList(set).contains(element);
	}

	private static HashSet<String> unionOf(String[]... sets) {
		HashSet<String> union = new HashSet<String>();
		for (String[] set : sets) {
			union.addAll(Arrays.asList(set));
		}
		return union;
	}
	
	static boolean isSpecialFunctionSymbol(String symbol){
		return specialFunctionSymbols.contains(symbol);
	}
	
	static HashSet<String> getAxioms(Tree formulaTree) {
		HashSet<String> axioms = new HashSet<String>();
		HashSet<Node> terms = formulaTree.getBinaryPredicates();
		for(Node term: terms){
			logger.info("Processing term: "+ term.getValue());
			axioms.addAll(getAxioms(term));
		}
		// FIXME: specific filename!
		axioms.add("general");
		return axioms;
	}
	
	private static HashSet<String> getAxioms(Node node) {
		HashSet<String> axioms = new HashSet<String>();

		if (node.isExponent()) {
			// FIXME:  Relying on matching axiom filename!
			axioms.add("pow");
		}
		if (isSpecialFunctionSymbol(node.getValue())){

		// Currently axiom file names match/resemble function names.
		// N.B. this is VERY fragile!
			if(containsElement(expLog, node.getValue())){
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-general");
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-extended");
			}

			if(containsElement(new String[]{"Sin", "Cos"}, node.getValue())){
				axioms.add(Operators.valueOf(node.getValue()).Tptp );
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-extended");
			}
			if(containsElement(new String[]{"Tan"}, node.getValue())){
				axioms.add(Operators.valueOf(node.getValue()).Tptp );
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-lower");
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-upper");
			}
			if(containsElement(hypTrigSym, node.getValue())){
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-lower");
				axioms.add(Operators.valueOf(node.getValue()).Tptp +"-upper");
			}

		}
		for(int i=0; i<node.getArity(); i++){
		axioms.addAll(getAxioms(node.getChildAt(i)));
		}
		return axioms;
	}
	
	public static String termToMetit(Term form, String name, String comments, boolean findInstance) {
		Tree formulaTree;
		if(findInstance){
			formulaTree = getFindInstance(form);
		}
		else{
			formulaTree = toMutableTree(form);
		}
		handleAltExp(formulaTree);
		handleBiImplication(formulaTree);
		String[] problem = treeToMetit(formulaTree);
		HashSet<String> axioms = getAxioms(formulaTree);

		return formatProblem(comments, name, problem, axioms);
	}
	
	public static String termToMetit(Term form, String name, boolean findInstance){
		return termToMetit(form,name,"Auto-generated MetiTarski problem", findInstance);
	}
	
	public static String termToMetit(Term form, boolean findInstance){
		return termToMetit(form, "Problem"+System.currentTimeMillis(), "Auto-generated MetiTarski problem", findInstance);
	}
	
	public static  Tree toMutableTree(Term form){
		
		if (form.op() == Op.FALSE) {
			logger.info("falsity");
			return new Tree(new Node("FALSUM"));
		} 
		else if (form.op() == Op.TRUE) {
			logger.info("truth");
			return new Tree(new Node("VERUM"));
		}
		
	/*	Constant symbols return a 1-element singleton tree,
	 *  with the constant symbol as its root/leaf. 
	 */
		if(form.arity()==0){
			return new Tree(new Node(processSymbol(form.op().name().toString())));
		  }
		  
	/*	Unary predicate symbols, such as -, and unary operators, such as ¬  
	 * 	as well as first-order quantifiers (∀,∃),
	 * 	return a tree with their respective symbol as the root, and recurse 
	 *	on the operand to add children.
	 */
		else if (form.arity() == 1) {
			Tree tree = new Tree(new Node(form.op().name().toString()));
			if (form.op() == Op.ALL || form.op() == Op.EX) {
				tree.getRootNode().addBoundVars(checkBoundVars(form, 0)); // Add variable(s) to the bound variable set.
			}
			tree.insertNodeInto(toMutableTree(form.sub(0)).getRootNode(),tree.getRootNode(), 0); // Recurse.
			return tree;
		}
	 
	/*	Binary predicate symbols (<,<=,=,>=,>), binary arithmetic operators (*,-,+,/,^),
	 * 	binary logical connectives (∧,∨,→)
	 *  return a (sub-)tree with their symbol at the root, and recurse on both operands
	 *  in sequence to compute the child elements.
	 */
		  else {
			  Tree tree = new Tree(new Node(form.op().name().toString()));
			  for(int i=0; i< form.arity(); i++){
			  tree.insertNodeInto(toMutableTree(form.sub(i)).getRootNode(), tree.getRootNode(),i);	
			  }
			  return tree;
		  }
	}
	
	/* Check for variables bound by the quantifier */
	private static TreeSet<String> checkBoundVars(Term form, int i) {
		TreeSet<String> boundVars = new TreeSet<String>();
		for (int j = 0, vbSize = form.varsBoundHere(i).size(); j < vbSize; j++) {
     		boundVars.add(processSymbol((form.varsBoundHere(i).get(j).name().toString())));
		}
		return boundVars;
	}
		
	/* Existentially quantify over the free variables.
	 * This is required for counterexample generation */
	
	private static Tree getFindInstance(Term form){
		Tree formulaTree = toMutableTree(form);
		// All variables in the formula
		TreeSet<String> freeVars = Tree.getFreeVars(formulaTree);
		for(String var: freeVars){
			logger.error("Free variable : " + var);
		}
		//FIXME: test this!
		Tree findInstanceTree = new Tree(new Node(Operators.exist.KeY));
		findInstanceTree.getRootNode().addBoundVars(freeVars);
		logger.error("Now bound : "+findInstanceTree.getRootNode().printBoundVars());
		findInstanceTree.insertNodeInto(formulaTree.getRootNode(), findInstanceTree.getRootNode(), 0);
		return findInstanceTree;
		
	} 
	
	
	private static String processSymbol(String var){
		// TPTP requirements
		return var.toUpperCase().replaceAll("\\$", "DOLLAR").replaceAll("_", "USCORE");
	}
	
	public static String[] treeToMetit(Tree formulaTree){
		Node root  =  formulaTree.getRootNode();
		return new String[]{ convert(root), Integer.toString(Tree.getVars(formulaTree).size())};
	}
	
	static String convert(Node node) {
		if(node.isVerum()){return Operators.VERUM.Tptp;}
		if(node.isFalsum()){return Operators.FALSUM.Tptp;}
		
		switch (node.getArity()) {
		case 0:
			return node.getValue();
		case 1:
			if (node.isQuantifier()) {
				return Operators.valueOf(node.getValue()).Tptp 
						+ "["+ node.printBoundVars() +"] : "
						+ convert(node.getFirstChild()) ;
			}
			else{
			return Operators.valueOf(node.getValue()).Tptp 
					+ "("
					+ convert(node.getChildAt(0)) 
					+ ")";
			}
		case 2:
			return "("+convert(node.getFirstChild()) 
					+ Operators.valueOf(node.getValue()).Tptp 
					+ convert(node.getSecondChild()) 
					+ ")";
		default: logger.error("No provision made for handling nodes with arities greater than 2 ! Children: ");
					for(int i=0; i<node.getArity(); i++){
						logger.error(node.getValue());
					}
		  		return node.getValue() + "[ARITY "+ node.getArity() +" ERROR]";
		}
	}
	
	static String formatProblem(String comments, String name, String[] problem, HashSet<String> axioms){
		StringBuilder output = new StringBuilder();
		
		for(String line: comments.trim().split("\n")){
			output.append("% "+ line + "\n");
		}
		output.append("% Number of variables: "+ problem[1]);
		output.append("\n");
		output.append("fof("+name+",conjecture, "+ problem[0] +").\n");
		
		for(String axiom: axioms){
			output.append("include('"+ axiom + ".ax').\n");
		}	
		
		return output.toString();
	}
	
	/******** Tree restructuring methods ********/
	
	static boolean isAltExp(Node node) {
		// Alternative exponential notation in Mathematica™
		if (node.isLeaf())
			return false;
		if (node.getValue() != null && node.getValue().equals("exp")
				&& node.getFirstChild().getValue().equals("E"))
			return true;
		return false;
	}
	
	static boolean isTrig(Node node){
		if(node.getValue()!= null && containsElement(trigSym, node.getValue())) return true;
		return false;
	}
	
	static Tree handleAltExp(Tree formulaTree){
		/* Method for converting Mathematica™-generated exponentials
		 * of the form :
		 *       ^
		 *     /   \
		 *    E    expr
		 * 
		 * to their equivalents in functional notation, i.e.  
		 * 
		 *       Exp
		 *        |
		 *       expr
		 *   
		 */
		
		handleAltExp(formulaTree.getRootNode());
		return formulaTree;
	}
	
	static boolean handleAltExp(Node node) {
		if (node.isLeaf())
			return false;
		if (isAltExp(node)) {
			node.setValue("Exp");
			node.removeFirstChild();
		} else {
			for (int i = 0; i < node.getArity(); i++) {
				handleAltExp(node.getChildAt(i));
			}
		}
		return false;
	}
	
	static Tree handleBiImplication(Tree formulaTree){
		/**
		 * Method for converting  bi-implication into a conjunction of implications.
		 * 
		 *          ↔
		 *         / \
		 *        A   B
		 * 
		 *          ∧
		 *         / \
		 *        /   \
		 *       /     \
		 *      →            → 
		 *     / \     / \
		 *    A   B   B   A
		 */ 
	
		handleBiImplication(formulaTree.getRootNode());
		return formulaTree;
	}
	
	static boolean handleBiImplication(Node node){
		if (node.isLeaf())
			return false;
		if (node.getValue().equals("equiv")) {
			// Create conjunct
			node.setValue("and");
			
			//First pair
			Tree A1 = Tree.cloneSubTree(node.getFirstChild());
			Tree B1 = Tree.cloneSubTree(node.getSecondChild());
			
			//Second pair
			Tree A2 = Tree.cloneSubTree(node.getFirstChild());
			Tree B2 = Tree.cloneSubTree(node.getSecondChild());
			
			node.removeAllChildren();
			logger.error("Converter sees arity: "+ node.getArity());
			
			// Form first implication
			node.addChildAt(0, new Node("imp"));
			logger.error("Added first child arity: "+ node.getArity());
			node.getFirstChild().addChildAt(0, A1.getRootNode());
			node.getFirstChild().addChildAt(1, B1.getRootNode());
			logger.error("Added  clones: "+ node.getArity());
			
			// Form second implication
			node.addChildAt(1, new Node("imp"));
			logger.error("Added second child arity: "+ node.getArity());
			node.getSecondChild().addChildAt(0, B2.getRootNode());
			node.getSecondChild().addChildAt(1, A2.getRootNode());
			logger.error("Added clones: "+ node.getArity());	
		}
		for (int i = 0; i < node.getArity(); i++) {
				handleBiImplication(node.getChildAt(i));
			}
		return true;
	}
}
